A:Type, B:(AType), eq:EqDecider(A), f, g, h:a:A fp B(a).
f  g  h = f  g  h  a:A fp B(a) 

latex

Definitions	x:A. B(x), a:A fp B(a), x(s), f  g, 1of(t), x  dom(f), f(x)?z, f(x), 2of(t), t  T, P  Q, P  Q, P & Q, P  Q, T, True, p  q, b, true, Prop, if b t else f fi, false, P  Q, {T}, , Unit, A, False,
Lemmas	l member wf, deq wf, append wf, filter wf, bnot wf, deq-member wf, append assoc, squash wf, true wf, filter append, filter filter, bool wf, iff transitivity, assert wf, eqtt to assert, assert-deq-member, member append, bfalse wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, btrue wf, band wf, member filter, or functionality wrt iff, and functionality wrt iff